FDL - Nuprl Definition : in-decl

Nuprl Definition : in-decl

0,22

InDecl(i) == ltg:{p:(IdLnk

Id)| destination(1of(p)) = i } fp

Type

clarification:

in-decl{i:l}(i) == ltg:{p:(IdLnk

Id)| destination(1of(p)) = i

Id } fp

Type{i}

Definitions a:A fp B(a), {x:A| B(x) }, x:AB(x), IdLnk, s = t, Id, destination(l), 1of(t), Type

FDL editor aliases in-decl

Definitions	a:A fp B(a), {x:A\| B(x) }, x:AB(x), IdLnk, s = t, Id, destination(l), 1of(t), Type
FDL editor aliases	in-decl